T:Type, L, L1, L2:T List.
interleaving(T;L1;L2;L)  {x, y:T. x before y  L1  x before y  L} 

latex

Definitions	t  T, x:A. B(x), ||as||, ij, P  Q, False, A, AB, , disjoint_sublists(T;L1;L2;L), Prop, P & Q, x before y  l, interleaving(T;L1;L2;L), {T}, True, T, L1  L2
Lemmas	disjoint sublists sublist, l before sublist, l before wf, nat wf, disjoint sublists wf, non neg length, length wf1